\begin{tabbing}
msga\{i:l\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$\+
\\[0ex]$\times$${\it da}$:$a$:Knd fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$
\\[0ex]$\times$$x$:Id fp$\rightarrow$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Void)
\\[0ex]$\times$$a$:Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;locl($a$))$\rightarrow$Prop$_{\mbox{\scriptsize i}}$
\\[0ex]$\times$${\it kx}$:Knd$\times$Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kx}$))$\rightarrow$fpf{-}cap(${\it ds}$;IdDeq;2of(${\it kx}$);Void)
\\[0ex]$\times$\=${\it kl}$:Knd$\times$IdLnk fp$\rightarrow$\+
\\[0ex](\=${\it tg}$:Id\+
\\[0ex]$\times$(\=State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kl}$))$\rightarrow$\+
\\[0ex](fpf{-}cap(${\it da}$;KindDeq;rcv(2of(${\it kl}$),${\it tg}$);Void) List))) List
\-\-\-\\[0ex]$\times$$x$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$${\it ltg}$:IdLnk$\times$Id fp$\rightarrow$ Knd List
\\[0ex]$\times$$k$:Knd fp$\rightarrow$ Id List
\\[0ex]$\times$$k$:Knd fp$\rightarrow$ IdLnk List
\\[0ex]$\times$$x$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$Top
\-
\end{tabbing}